T:(IdIdType), V:(IdKndType), a:(i, x:Id. AtomFree(Type;T(i,x))),
b:(i:Id, k:Knd. AtomFree(Type;V(i,k))).
<a,b>  ESAtomAxiom{i:l}(T;V) 

latex

Definitions	Type, t  T, Id, x:AB(x), Knd, f(a), x:A. B(x), AtomFree(T;x), Prop, x:AB(x), <a,b>, ESAtomAxiom{i:l}(T;V)
Lemmas	atom-free wf, Knd wf, Id wf